The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

r(r(x1)) → s(r(x1))
r(s(x1)) → s(r(x1))
r(n(x1)) → s(r(x1))
r(b(x1)) → u(s(b(x1)))
r(u(x1)) → u(r(x1))
s(u(x1)) → u(s(x1))
n(u(x1)) → u(n(x1))
t(r(u(x1))) → t(c(r(x1)))
t(s(u(x1))) → t(c(r(x1)))
t(n(u(x1))) → t(c(r(x1)))
c(u(x1)) → u(c(x1))
c(s(x1)) → s(c(x1))
c(r(x1)) → r(c(x1))
c(n(x1)) → n(c(x1))
c(n(x1)) → n(x1)

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(r(z0)) → c1(S(r(z0)), R(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
R(b(z0)) → c4(S(b(z0)))
R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
T(r(u(z0))) → c8(T(c(r(z0))), C(r(z0)), R(z0))
T(s(u(z0))) → c9(T(c(r(z0))), C(r(z0)), R(z0))
T(n(u(z0))) → c10(T(c(r(z0))), C(r(z0)), R(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(R(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))

S tuples:

R(r(z0)) → c1(S(r(z0)), R(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
R(b(z0)) → c4(S(b(z0)))
R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
T(r(u(z0))) → c8(T(c(r(z0))), C(r(z0)), R(z0))
T(s(u(z0))) → c9(T(c(r(z0))), C(r(z0)), R(z0))
T(n(u(z0))) → c10(T(c(r(z0))), C(r(z0)), R(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(R(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))

K tuples:none
Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, T, C

Compound Symbols:

c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15

(3) CdtUnreachableProof (EQUIVALENT transformation)

The following tuples could be removed as they are not reachable from basic start terms:

T(r(u(z0))) → c8(T(c(r(z0))), C(r(z0)), R(z0))
T(s(u(z0))) → c9(T(c(r(z0))), C(r(z0)), R(z0))
T(n(u(z0))) → c10(T(c(r(z0))), C(r(z0)), R(z0))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(b(z0)) → c4(S(b(z0)))
R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(R(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(r(z0)) → c1(S(r(z0)), R(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))

S tuples:

R(r(z0)) → c1(S(r(z0)), R(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
R(b(z0)) → c4(S(b(z0)))
R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(R(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))

K tuples:none
Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c4, c5, c6, c7, c11, c12, c13, c14, c15, c1, c2, c3

(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 1 of 12 dangling nodes:

R(b(z0)) → c4(S(b(z0)))

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(R(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(r(z0)) → c1(S(r(z0)), R(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))

S tuples:

R(r(z0)) → c1(S(r(z0)), R(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(R(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))

K tuples:none
Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c13, c14, c15, c1, c2, c3

(7) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)

Removed 2 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

K tuples:none
Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(9) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

C(n(z0)) → c15(N(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [4]   
POL(N(x₁)) = 0   
POL(R(x₁)) = 0   
POL(S(x₁)) = 0   
POL(b(x₁)) = [4] + x₁   
POL(c(x₁)) = [3] + [3]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [5]x₁   
POL(r(x₁)) = [4]x₁   
POL(s(x₁)) = [2]x₁   
POL(u(x₁)) = [5]   

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

K tuples:

C(n(z0)) → c15(N(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

R(u(z0)) → c5(R(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [5]   
POL(N(x₁)) = 0   
POL(R(x₁)) = [2]x₁   
POL(S(x₁)) = 0   
POL(b(x₁)) = [4]   
POL(c(x₁)) = [3]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [4]x₁   
POL(r(x₁)) = [4]x₁   
POL(s(x₁)) = x₁   
POL(u(x₁)) = [1] + x₁   

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

C(u(z0)) → c11(C(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [3] + x₁   
POL(N(x₁)) = 0   
POL(R(x₁)) = 0   
POL(S(x₁)) = 0   
POL(b(x₁)) = [4]   
POL(c(x₁)) = [5]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = x₁   
POL(r(x₁)) = [4]x₁   
POL(s(x₁)) = x₁   
POL(u(x₁)) = [1] + x₁   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))
C(u(z0)) → c11(C(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

R(n(z0)) → c3(S(r(z0)), R(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [5]   
POL(N(x₁)) = 0   
POL(R(x₁)) = [4]x₁   
POL(S(x₁)) = 0   
POL(b(x₁)) = [4] + x₁   
POL(c(x₁)) = [3] + [3]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [1] + [3]x₁   
POL(r(x₁)) = [4]x₁   
POL(s(x₁)) = x₁   
POL(u(x₁)) = [1] + x₁   

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))
C(u(z0)) → c11(C(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

N(u(z0)) → c7(N(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [3] + [2]x₁   
POL(N(x₁)) = [4] + [4]x₁   
POL(R(x₁)) = 0   
POL(S(x₁)) = 0   
POL(b(x₁)) = [4]   
POL(c(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [4] + [3]x₁   
POL(r(x₁)) = [4]x₁   
POL(s(x₁)) = x₁   
POL(u(x₁)) = [1] + x₁   

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
S(u(z0)) → c6(S(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))
C(u(z0)) → c11(C(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
N(u(z0)) → c7(N(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

R(r(z0)) → c1(R(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [3]   
POL(N(x₁)) = 0   
POL(R(x₁)) = x₁   
POL(S(x₁)) = 0   
POL(b(x₁)) = [2]   
POL(c(x₁)) = [1] + [4]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [1] + [4]x₁   
POL(r(x₁)) = [1] + [2]x₁   
POL(s(x₁)) = [4] + [3]x₁   
POL(u(x₁)) = x₁   

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
S(u(z0)) → c6(S(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))

K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))
C(u(z0)) → c11(C(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
N(u(z0)) → c7(N(z0))
R(r(z0)) → c1(R(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

C(n(z0)) → c14(N(c(z0)), C(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [3] + x₁   
POL(N(x₁)) = [1]   
POL(R(x₁)) = 0   
POL(S(x₁)) = 0   
POL(b(x₁)) = [4]   
POL(c(x₁)) = [5] + [2]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [2] + x₁   
POL(r(x₁)) = [4]x₁   
POL(s(x₁)) = x₁   
POL(u(x₁)) = [1] + x₁   

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
S(u(z0)) → c6(S(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))

K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))
C(u(z0)) → c11(C(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
N(u(z0)) → c7(N(z0))
R(r(z0)) → c1(R(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

C(s(z0)) → c12(S(c(z0)), C(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [4]x₁   
POL(N(x₁)) = [3]   
POL(R(x₁)) = 0   
POL(S(x₁)) = 0   
POL(b(x₁)) = [4] + x₁   
POL(c(x₁)) = [2] + [3]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [2] + [3]x₁   
POL(r(x₁)) = [4] + [4]x₁   
POL(s(x₁)) = [5] + x₁   
POL(u(x₁)) = [4] + x₁   

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
S(u(z0)) → c6(S(z0))
C(r(z0)) → c13(C(z0))

K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))
C(u(z0)) → c11(C(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
N(u(z0)) → c7(N(z0))
R(r(z0)) → c1(R(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(25) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

C(r(z0)) → c13(C(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [5] + [2]x₁   
POL(N(x₁)) = [2]   
POL(R(x₁)) = 0   
POL(S(x₁)) = 0   
POL(b(x₁)) = [4]   
POL(c(x₁)) = [2]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [3] + [4]x₁   
POL(r(x₁)) = [4] + [4]x₁   
POL(s(x₁)) = [4] + x₁   
POL(u(x₁)) = [5] + x₁   

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

R(s(z0)) → c2(S(r(z0)), R(z0))
S(u(z0)) → c6(S(z0))

K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))
C(u(z0)) → c11(C(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
N(u(z0)) → c7(N(z0))
R(r(z0)) → c1(R(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(27) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

R(s(z0)) → c2(S(r(z0)), R(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [2] + x₁   
POL(N(x₁)) = [2]   
POL(R(x₁)) = [2]x₁   
POL(S(x₁)) = [2]   
POL(b(x₁)) = [4]   
POL(c(x₁)) = [1] + [4]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [2] + [4]x₁   
POL(r(x₁)) = [4] + [4]x₁   
POL(s(x₁)) = [5] + x₁   
POL(u(x₁)) = [4] + x₁   

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:

S(u(z0)) → c6(S(z0))

K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))
C(u(z0)) → c11(C(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
N(u(z0)) → c7(N(z0))
R(r(z0)) → c1(R(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(29) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

S(u(z0)) → c6(S(z0))

We considered the (Usable) Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
s(u(z0)) → u(s(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)
n(u(z0)) → u(n(z0))

And the Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(C(x₁)) = [5] + [4]x₁   
POL(N(x₁)) = x₁   
POL(R(x₁)) = [4]x₁   
POL(S(x₁)) = [3] + x₁   
POL(b(x₁)) = [4] + x₁   
POL(c(x₁)) = [3] + [4]x₁   
POL(c1(x₁)) = x₁   
POL(c11(x₁)) = x₁   
POL(c12(x₁, x₂)) = x₁ + x₂   
POL(c13(x₁)) = x₁   
POL(c14(x₁, x₂)) = x₁ + x₂   
POL(c15(x₁)) = x₁   
POL(c2(x₁, x₂)) = x₁ + x₂   
POL(c3(x₁, x₂)) = x₁ + x₂   
POL(c5(x₁)) = x₁   
POL(c6(x₁)) = x₁   
POL(c7(x₁)) = x₁   
POL(n(x₁)) = [4] + [5]x₁   
POL(r(x₁)) = [4] + [3]x₁   
POL(s(x₁)) = [4] + [2]x₁   
POL(u(x₁)) = [1] + x₁   

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

r(r(z0)) → s(r(z0))
r(s(z0)) → s(r(z0))
r(n(z0)) → s(r(z0))
r(b(z0)) → u(s(b(z0)))
r(u(z0)) → u(r(z0))
s(u(z0)) → u(s(z0))
n(u(z0)) → u(n(z0))
t(r(u(z0))) → t(c(r(z0)))
t(s(u(z0))) → t(c(r(z0)))
t(n(u(z0))) → t(c(r(z0)))
c(u(z0)) → u(c(z0))
c(s(z0)) → s(c(z0))
c(r(z0)) → r(c(z0))
c(n(z0)) → n(c(z0))
c(n(z0)) → n(z0)

Tuples:

R(u(z0)) → c5(R(z0))
S(u(z0)) → c6(S(z0))
N(u(z0)) → c7(N(z0))
C(u(z0)) → c11(C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(n(z0)) → c15(N(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
C(r(z0)) → c13(C(z0))
R(r(z0)) → c1(R(z0))

S tuples:none
K tuples:

C(n(z0)) → c15(N(z0))
R(u(z0)) → c5(R(z0))
C(u(z0)) → c11(C(z0))
R(n(z0)) → c3(S(r(z0)), R(z0))
N(u(z0)) → c7(N(z0))
R(r(z0)) → c1(R(z0))
C(n(z0)) → c14(N(c(z0)), C(z0))
C(s(z0)) → c12(S(c(z0)), C(z0))
C(r(z0)) → c13(C(z0))
R(s(z0)) → c2(S(r(z0)), R(z0))
S(u(z0)) → c6(S(z0))

Defined Rule Symbols:

r, s, n, t, c

Defined Pair Symbols:

R, S, N, C

Compound Symbols:

c5, c6, c7, c11, c12, c14, c15, c2, c3, c13, c1

(31) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(32) BOUNDS(O(1), O(1))